H-Termination proof of /home/matraf/haskell/eval_FullyBlown

MAYBE 2.123 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could not be shown:

↳ HASKELL

  ↳ LR

mainModule Monad

((foldM_ :: Monad b => (c -> a -> b c) -> c -> [a] -> b ()) :: Monad b => (c -> a -> b c) -> c -> [a] -> b ())

module Monad where

import qualified Maybe
import qualified Prelude

foldM :: Monad b => (a -> c -> b a) -> a -> [c] -> b a

foldM	_ a []	=	return a
foldM	f a (x : xs)	=	f a x >>= (\fax ->foldM f fax xs)

foldM_ :: Monad a => (c -> b -> a c) -> c -> [b] -> a ()

foldM_

f a xs

foldM f a xs >> return ()

module Maybe where

import qualified Monad
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\fax→foldM f fax xs

is transformed to

foldM0 f xs fax = foldM f fax xs

The following Lambda expression

\_→q

is transformed to

gtGt0 q _ = q

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Monad

((foldM_ :: Monad a => (b -> c -> a b) -> b -> [c] -> a ()) :: Monad a => (b -> c -> a b) -> b -> [c] -> a ())

module Maybe where

import qualified Monad
import qualified Prelude

module Monad where

import qualified Maybe
import qualified Prelude

foldM :: Monad c => (a -> b -> c a) -> a -> [b] -> c a

foldM	_ a []	=	return a
foldM	f a (x : xs)	=	f a x >>= foldM0 f xs

foldM0

f xs fax

foldM f fax xs

foldM_ :: Monad b => (c -> a -> b c) -> c -> [a] -> b ()

foldM_

f a xs

foldM f a xs >> return ()

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Monad

((foldM_ :: Monad a => (b -> c -> a b) -> b -> [c] -> a ()) :: Monad a => (b -> c -> a b) -> b -> [c] -> a ())

module Monad where

import qualified Maybe
import qualified Prelude

foldM :: Monad a => (c -> b -> a c) -> c -> [b] -> a c

foldM	vw a []	=	return a
foldM	f a (x : xs)	=	f a x >>= foldM0 f xs

foldM0

f xs fax

foldM f fax xs

foldM_ :: Monad a => (b -> c -> a b) -> b -> [c] -> a ()

foldM_

f a xs

foldM f a xs >> return ()

module Maybe where

import qualified Monad
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

mainModule Monad

(foldM_ :: Monad b => (a -> c -> b a) -> a -> [c] -> b ())

module Maybe where

import qualified Monad
import qualified Prelude

module Monad where

import qualified Maybe
import qualified Prelude

foldM :: Monad a => (b -> c -> a b) -> b -> [c] -> a b

foldM	vw a []	=	return a
foldM	f a (x : xs)	=	f a x >>= foldM0 f xs

foldM0

f xs fax

foldM f fax xs

foldM_ :: Monad a => (c -> b -> a c) -> c -> [b] -> a ()

foldM_

f a xs

foldM f a xs >> return ()

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="foldM_\n  Monad a",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="foldM_ wu3\n  Monad a",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="foldM_ wu3 wu4\n  Monad a",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="foldM_ wu3 wu4 wu5\n  Monad a",fontsize=16,color="black",shape="triangle"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="foldM wu3 wu4 wu5 >> return ()\n  Monad a",fontsize=16,color="blue",shape="box"];637[label=">> :: (IO a) -> (IO ()) -> IO ()",fontsize=10,color="white",style="solid",shape="box"];6 -> 637[label="",style="solid", color="blue", weight=9];
637 -> 7[label="",style="solid", color="blue", weight=3];
638[label=">> :: (Maybe a) -> (Maybe ()) -> Maybe ()",fontsize=10,color="white",style="solid",shape="box"];6 -> 638[label="",style="solid", color="blue", weight=9];
638 -> 8[label="",style="solid", color="blue", weight=3];
639[label=">> :: ([] a) -> ([] ()) -> [] ()",fontsize=10,color="white",style="solid",shape="box"];6 -> 639[label="",style="solid", color="blue", weight=9];
639 -> 9[label="",style="solid", color="blue", weight=3];
7[label="foldM wu3 wu4 wu5 >> return ()",fontsize=16,color="black",shape="box"];7 -> 10[label="",style="solid", color="black", weight=3];
8[label="foldM wu3 wu4 wu5 >> return ()",fontsize=16,color="black",shape="box"];8 -> 11[label="",style="solid", color="black", weight=3];
9[label="foldM wu3 wu4 wu5 >> return ()",fontsize=16,color="black",shape="box"];9 -> 12[label="",style="solid", color="black", weight=3];
10[label="foldM wu3 wu4 wu5 >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="foldM wu3 wu4 wu5 >>= gtGt0 (return ())",fontsize=16,color="burlywood",shape="triangle"];640[label="wu5/wu50 : wu51",fontsize=10,color="white",style="solid",shape="box"];11 -> 640[label="",style="solid", color="burlywood", weight=9];
640 -> 14[label="",style="solid", color="burlywood", weight=3];
641[label="wu5/[]",fontsize=10,color="white",style="solid",shape="box"];11 -> 641[label="",style="solid", color="burlywood", weight=9];
641 -> 15[label="",style="solid", color="burlywood", weight=3];
12 -> 522[label="",style="dashed", color="red", weight=0];
12[label="foldM wu3 wu4 wu5 >>= gtGt0 (return ())",fontsize=16,color="magenta"];12 -> 523[label="",style="dashed", color="magenta", weight=3];
13[label="primbindIO (foldM wu3 wu4 wu5) (gtGt0 (return ()))",fontsize=16,color="black",shape="box"];13 -> 18[label="",style="solid", color="black", weight=3];
14[label="foldM wu3 wu4 (wu50 : wu51) >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];14 -> 19[label="",style="solid", color="black", weight=3];
15[label="foldM wu3 wu4 [] >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];15 -> 20[label="",style="solid", color="black", weight=3];
523[label="foldM wu3 wu4 wu5",fontsize=16,color="burlywood",shape="triangle"];643[label="wu5/wu50 : wu51",fontsize=10,color="white",style="solid",shape="box"];523 -> 643[label="",style="solid", color="burlywood", weight=9];
643 -> 577[label="",style="solid", color="burlywood", weight=3];
644[label="wu5/[]",fontsize=10,color="white",style="solid",shape="box"];523 -> 644[label="",style="solid", color="burlywood", weight=9];
644 -> 578[label="",style="solid", color="burlywood", weight=3];
522[label="wu38 >>= gtGt0 (return ())",fontsize=16,color="burlywood",shape="triangle"];645[label="wu38/wu380 : wu381",fontsize=10,color="white",style="solid",shape="box"];522 -> 645[label="",style="solid", color="burlywood", weight=9];
645 -> 579[label="",style="solid", color="burlywood", weight=3];
646[label="wu38/[]",fontsize=10,color="white",style="solid",shape="box"];522 -> 646[label="",style="solid", color="burlywood", weight=9];
646 -> 580[label="",style="solid", color="burlywood", weight=3];
18[label="terminator (foldM wu3 wu4 wu5) (gtGt0 (return ()))",fontsize=16,color="black",shape="box"];18 -> 23[label="",style="solid", color="black", weight=3];
19 -> 24[label="",style="dashed", color="red", weight=0];
19[label="wu3 wu4 wu50 >>= foldM0 wu3 wu51 >>= gtGt0 (return ())",fontsize=16,color="magenta"];19 -> 25[label="",style="dashed", color="magenta", weight=3];
20[label="return wu4 >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];20 -> 26[label="",style="solid", color="black", weight=3];
577[label="foldM wu3 wu4 (wu50 : wu51)",fontsize=16,color="black",shape="box"];577 -> 581[label="",style="solid", color="black", weight=3];
578[label="foldM wu3 wu4 []",fontsize=16,color="black",shape="box"];578 -> 582[label="",style="solid", color="black", weight=3];
579[label="wu380 : wu381 >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];579 -> 583[label="",style="solid", color="black", weight=3];
580[label="[] >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];580 -> 584[label="",style="solid", color="black", weight=3];
23[label="ter0m (foldM wu3 wu4 wu5) (gtGt0 (return ()))",fontsize=16,color="green",shape="box"];23 -> 30[label="",style="dashed", color="green", weight=3];
23 -> 31[label="",style="dashed", color="green", weight=3];
25[label="wu3 wu4 wu50",fontsize=16,color="green",shape="box"];25 -> 32[label="",style="dashed", color="green", weight=3];
25 -> 33[label="",style="dashed", color="green", weight=3];
24[label="wu6 >>= foldM0 wu3 wu51 >>= gtGt0 (return ())",fontsize=16,color="burlywood",shape="triangle"];648[label="wu6/Nothing",fontsize=10,color="white",style="solid",shape="box"];24 -> 648[label="",style="solid", color="burlywood", weight=9];
648 -> 34[label="",style="solid", color="burlywood", weight=3];
649[label="wu6/Just wu60",fontsize=10,color="white",style="solid",shape="box"];24 -> 649[label="",style="solid", color="burlywood", weight=9];
649 -> 35[label="",style="solid", color="burlywood", weight=3];
26[label="Just wu4 >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];26 -> 36[label="",style="solid", color="black", weight=3];
581 -> 585[label="",style="dashed", color="red", weight=0];
581[label="wu3 wu4 wu50 >>= foldM0 wu3 wu51",fontsize=16,color="magenta"];581 -> 586[label="",style="dashed", color="magenta", weight=3];
582[label="return wu4",fontsize=16,color="black",shape="triangle"];582 -> 587[label="",style="solid", color="black", weight=3];
583 -> 609[label="",style="dashed", color="red", weight=0];
583[label="gtGt0 (return ()) wu380 ++ (wu381 >>= gtGt0 (return ()))",fontsize=16,color="magenta"];583 -> 610[label="",style="dashed", color="magenta", weight=3];
583 -> 611[label="",style="dashed", color="magenta", weight=3];
584[label="[]",fontsize=16,color="green",shape="box"];30[label="foldM wu3 wu4 wu5",fontsize=16,color="burlywood",shape="triangle"];652[label="wu5/wu50 : wu51",fontsize=10,color="white",style="solid",shape="box"];30 -> 652[label="",style="solid", color="burlywood", weight=9];
652 -> 44[label="",style="solid", color="burlywood", weight=3];
653[label="wu5/[]",fontsize=10,color="white",style="solid",shape="box"];30 -> 653[label="",style="solid", color="burlywood", weight=9];
653 -> 45[label="",style="solid", color="burlywood", weight=3];
31[label="gtGt0 (return ())",fontsize=16,color="grey",shape="box"];31 -> 46[label="",style="dashed", color="grey", weight=3];
32[label="wu4",fontsize=16,color="green",shape="box"];33[label="wu50",fontsize=16,color="green",shape="box"];34[label="Nothing >>= foldM0 wu3 wu51 >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];34 -> 47[label="",style="solid", color="black", weight=3];
35[label="Just wu60 >>= foldM0 wu3 wu51 >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];35 -> 48[label="",style="solid", color="black", weight=3];
36[label="gtGt0 (return ()) wu4",fontsize=16,color="black",shape="box"];36 -> 49[label="",style="solid", color="black", weight=3];
586[label="wu3 wu4 wu50",fontsize=16,color="green",shape="box"];586 -> 591[label="",style="dashed", color="green", weight=3];
586 -> 592[label="",style="dashed", color="green", weight=3];
585[label="wu39 >>= foldM0 wu3 wu51",fontsize=16,color="burlywood",shape="triangle"];654[label="wu39/wu390 : wu391",fontsize=10,color="white",style="solid",shape="box"];585 -> 654[label="",style="solid", color="burlywood", weight=9];
654 -> 593[label="",style="solid", color="burlywood", weight=3];
655[label="wu39/[]",fontsize=10,color="white",style="solid",shape="box"];585 -> 655[label="",style="solid", color="burlywood", weight=9];
655 -> 594[label="",style="solid", color="burlywood", weight=3];
587[label="wu4 : []",fontsize=16,color="green",shape="box"];610 -> 522[label="",style="dashed", color="red", weight=0];
610[label="wu381 >>= gtGt0 (return ())",fontsize=16,color="magenta"];610 -> 622[label="",style="dashed", color="magenta", weight=3];
611 -> 623[label="",style="dashed", color="red", weight=0];
611[label="gtGt0 (return ()) wu380",fontsize=16,color="magenta"];611 -> 624[label="",style="dashed", color="magenta", weight=3];
609[label="wu44 ++ wu43",fontsize=16,color="burlywood",shape="triangle"];658[label="wu44/wu440 : wu441",fontsize=10,color="white",style="solid",shape="box"];609 -> 658[label="",style="solid", color="burlywood", weight=9];
658 -> 625[label="",style="solid", color="burlywood", weight=3];
659[label="wu44/[]",fontsize=10,color="white",style="solid",shape="box"];609 -> 659[label="",style="solid", color="burlywood", weight=9];
659 -> 626[label="",style="solid", color="burlywood", weight=3];
44[label="foldM wu3 wu4 (wu50 : wu51)",fontsize=16,color="black",shape="box"];44 -> 53[label="",style="solid", color="black", weight=3];
45[label="foldM wu3 wu4 []",fontsize=16,color="black",shape="box"];45 -> 54[label="",style="solid", color="black", weight=3];
46[label="gtGt0 (return ()) wu8",fontsize=16,color="black",shape="triangle"];46 -> 55[label="",style="solid", color="black", weight=3];
47[label="Nothing >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];47 -> 56[label="",style="solid", color="black", weight=3];
48[label="foldM0 wu3 wu51 wu60 >>= gtGt0 (return ())",fontsize=16,color="black",shape="box"];48 -> 57[label="",style="solid", color="black", weight=3];
49[label="return ()",fontsize=16,color="black",shape="box"];49 -> 58[label="",style="solid", color="black", weight=3];
591[label="wu4",fontsize=16,color="green",shape="box"];592[label="wu50",fontsize=16,color="green",shape="box"];593[label="wu390 : wu391 >>= foldM0 wu3 wu51",fontsize=16,color="black",shape="box"];593 -> 598[label="",style="solid", color="black", weight=3];
594[label="[] >>= foldM0 wu3 wu51",fontsize=16,color="black",shape="box"];594 -> 599[label="",style="solid", color="black", weight=3];
622[label="wu381",fontsize=16,color="green",shape="box"];624 -> 582[label="",style="dashed", color="red", weight=0];
624[label="return ()",fontsize=16,color="magenta"];624 -> 627[label="",style="dashed", color="magenta", weight=3];
623[label="gtGt0 wu45 wu380",fontsize=16,color="black",shape="triangle"];623 -> 628[label="",style="solid", color="black", weight=3];
625[label="(wu440 : wu441) ++ wu43",fontsize=16,color="black",shape="box"];625 -> 631[label="",style="solid", color="black", weight=3];
626[label="[] ++ wu43",fontsize=16,color="black",shape="box"];626 -> 632[label="",style="solid", color="black", weight=3];
53[label="wu3 wu4 wu50 >>= foldM0 wu3 wu51",fontsize=16,color="black",shape="box"];53 -> 63[label="",style="solid", color="black", weight=3];
54[label="return wu4",fontsize=16,color="black",shape="triangle"];54 -> 64[label="",style="solid", color="black", weight=3];
55 -> 54[label="",style="dashed", color="red", weight=0];
55[label="return ()",fontsize=16,color="magenta"];55 -> 65[label="",style="dashed", color="magenta", weight=3];
56[label="Nothing",fontsize=16,color="green",shape="box"];57 -> 11[label="",style="dashed", color="red", weight=0];
57[label="foldM wu3 wu60 wu51 >>= gtGt0 (return ())",fontsize=16,color="magenta"];57 -> 66[label="",style="dashed", color="magenta", weight=3];
57 -> 67[label="",style="dashed", color="magenta", weight=3];
58[label="Just ()",fontsize=16,color="green",shape="box"];598 -> 609[label="",style="dashed", color="red", weight=0];
598[label="foldM0 wu3 wu51 wu390 ++ (wu391 >>= foldM0 wu3 wu51)",fontsize=16,color="magenta"];598 -> 616[label="",style="dashed", color="magenta", weight=3];
598 -> 617[label="",style="dashed", color="magenta", weight=3];
599[label="[]",fontsize=16,color="green",shape="box"];627[label="()",fontsize=16,color="green",shape="box"];628[label="wu45",fontsize=16,color="green",shape="box"];631[label="wu440 : wu441 ++ wu43",fontsize=16,color="green",shape="box"];631 -> 635[label="",style="dashed", color="green", weight=3];
632[label="wu43",fontsize=16,color="green",shape="box"];63[label="primbindIO (wu3 wu4 wu50) (foldM0 wu3 wu51)",fontsize=16,color="black",shape="box"];63 -> 71[label="",style="solid", color="black", weight=3];
64[label="primretIO wu4",fontsize=16,color="black",shape="box"];64 -> 72[label="",style="solid", color="black", weight=3];
65[label="()",fontsize=16,color="green",shape="box"];66[label="wu60",fontsize=16,color="green",shape="box"];67[label="wu51",fontsize=16,color="green",shape="box"];616 -> 585[label="",style="dashed", color="red", weight=0];
616[label="wu391 >>= foldM0 wu3 wu51",fontsize=16,color="magenta"];616 -> 629[label="",style="dashed", color="magenta", weight=3];
617[label="foldM0 wu3 wu51 wu390",fontsize=16,color="black",shape="box"];617 -> 630[label="",style="solid", color="black", weight=3];
635 -> 609[label="",style="dashed", color="red", weight=0];
635[label="wu441 ++ wu43",fontsize=16,color="magenta"];635 -> 636[label="",style="dashed", color="magenta", weight=3];
71[label="terminator (wu3 wu4 wu50) (foldM0 wu3 wu51)",fontsize=16,color="black",shape="box"];71 -> 76[label="",style="solid", color="black", weight=3];
72[label="terminator wu4",fontsize=16,color="black",shape="box"];72 -> 77[label="",style="solid", color="black", weight=3];
629[label="wu391",fontsize=16,color="green",shape="box"];630 -> 523[label="",style="dashed", color="red", weight=0];
630[label="foldM wu3 wu390 wu51",fontsize=16,color="magenta"];630 -> 633[label="",style="dashed", color="magenta", weight=3];
630 -> 634[label="",style="dashed", color="magenta", weight=3];
636[label="wu441",fontsize=16,color="green",shape="box"];76[label="ter1m (wu3 wu4 wu50) (foldM0 wu3 wu51)",fontsize=16,color="green",shape="box"];76 -> 82[label="",style="dashed", color="green", weight=3];
76 -> 83[label="",style="dashed", color="green", weight=3];
77[label="ter2m wu4",fontsize=16,color="green",shape="box"];77 -> 84[label="",style="dashed", color="green", weight=3];
633[label="wu390",fontsize=16,color="green",shape="box"];634[label="wu51",fontsize=16,color="green",shape="box"];82[label="wu3 wu4 wu50",fontsize=16,color="green",shape="box"];82 -> 93[label="",style="dashed", color="green", weight=3];
82 -> 94[label="",style="dashed", color="green", weight=3];
83[label="foldM0 wu3 wu51",fontsize=16,color="grey",shape="box"];83 -> 95[label="",style="dashed", color="grey", weight=3];
84[label="wu4",fontsize=16,color="green",shape="box"];93[label="wu4",fontsize=16,color="green",shape="box"];94[label="wu50",fontsize=16,color="green",shape="box"];95[label="foldM0 wu3 wu51 wu11",fontsize=16,color="black",shape="triangle"];95 -> 99[label="",style="solid", color="black", weight=3];
99 -> 30[label="",style="dashed", color="red", weight=0];
99[label="foldM wu3 wu11 wu51",fontsize=16,color="magenta"];99 -> 103[label="",style="dashed", color="magenta", weight=3];
99 -> 104[label="",style="dashed", color="magenta", weight=3];
103[label="wu11",fontsize=16,color="green",shape="box"];104[label="wu51",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(wu440, wu441), wu43, h) → new_psPs(wu441, wu43, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_psPs(:(wu440, wu441), wu43, h) → new_psPs(wu441, wu43, h)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ UsableRulesReductionPairsProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs(wu3, wu51, h, ba) → new_gtGtEs(wu3, wu51, h, ba)
new_foldM(wu3, :(wu50, wu51), h, ba) → new_gtGtEs(wu3, wu51, h, ba)
new_gtGtEs(wu3, wu51, h, ba) → new_foldM(wu3, wu51, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

new_foldM(wu3, :(wu50, wu51), h, ba) → new_gtGtEs(wu3, wu51, h, ba)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [25]:

POL(:(x₁, x₂)) = x₁ + 2·x₂
POL(new_foldM(x₁, x₂, x₃, x₄)) = 2 + x₁ + x₂ + x₃ + x₄
POL(new_gtGtEs(x₁, x₂, x₃, x₄)) = 2 + x₁ + 2·x₂ + x₃ + x₄

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ UsableRulesReductionPairsProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs(wu3, wu51, h, ba) → new_gtGtEs(wu3, wu51, h, ba)
new_gtGtEs(wu3, wu51, h, ba) → new_foldM(wu3, wu51, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ UsableRulesReductionPairsProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ NonTerminationProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs(wu3, wu51, h, ba) → new_gtGtEs(wu3, wu51, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_gtGtEs(wu3, wu51, h, ba) → new_gtGtEs(wu3, wu51, h, ba)

The TRS R consists of the following rules:none

s = new_gtGtEs(wu3, wu51, h, ba) evaluates to t =new_gtGtEs(wu3, wu51, h, ba)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_gtGtEs(wu3, wu51, h, ba) to new_gtGtEs(wu3, wu51, h, ba).

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs0(:(wu380, wu381), h) → new_gtGtEs0(wu381, h)

From the DPs we obtained the following set of size-change graphs:

new_gtGtEs0(:(wu380, wu381), h) → new_gtGtEs0(wu381, h)
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs2(wu3, :(wu50, wu51), h, ba) → new_gtGtEs1(wu3, wu51, h, ba)
new_gtGtEs1(wu3, wu51, h, ba) → new_gtGtEs2(wu3, wu51, h, ba)

From the DPs we obtained the following set of size-change graphs:

new_gtGtEs1(wu3, wu51, h, ba) → new_gtGtEs2(wu3, wu51, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
new_gtGtEs2(wu3, :(wu50, wu51), h, ba) → new_gtGtEs1(wu3, wu51, h, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_foldM1(wu3, :(wu50, wu51), h, ba) → new_foldM1(wu3, wu51, h, ba)
new_foldM0(wu3, wu51, wu11, h, ba) → new_foldM1(wu3, wu51, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_foldM1(wu3, :(wu50, wu51), h, ba) → new_foldM1(wu3, wu51, h, ba)

From the DPs we obtained the following set of size-change graphs:

new_foldM1(wu3, :(wu50, wu51), h, ba) → new_foldM1(wu3, wu51, h, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4

Haskell To QDPs

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ DependencyGraphProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs1(Just(wu60), wu3, wu51, h, ba, []) → new_gtGtEs2(wu3, wu60, wu51, h, ba, [])

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_foldM0(wu3, wu51, wu11, h, ba, []) → new_foldM1(wu3, wu11, wu51, h, ba, [])

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.